(* A structure which contains the relevant identifiers and letctions of the Naive algorithm implementation,
   adapted from the DICE 2010 paper. The algorithm pseudo-code can be found in "naive_algorithm.docx" *)
module NAIVE_ANALYSIS_ALGORITHM
open BJK_ALGORITHM
open FSEvent
open setOfPairs

(* composition operator for context-graphs *)
let (@@) g1 g2 = ContextGraph.compose g1 g2

(* LUB (join) operator for context-graphs *)

let (|||) g1 g2 = ContextGraph.joinAsLeastUpperBound g1 g2

type DebugInfoAddedEventArgs(text : string) =
    inherit System.EventArgs()
    member x.Text = text

let debugInfoAdded = new Event<DebugInfoAddedEventArgs>()

(* type AbstractInterpreter encapsulates the abstract interpreter algorithm, as described in abstractInterpreterAlgorithm.docx *)
type NaiveAnalysis(analysis_params : Analysis.ANALYSIS_PARMS) =
    let Debug = ref true

    [<CLIEvent>]
    member x.CommandGraphUpdated = commandGraphUpdated.Publish

    [<CLIEvent>]
    member x.DebugInfoAdded = debugInfoAdded.Publish

    (* the entry point for the abstact interpreter execution. Recieves a command of the core language as input (in AST form) and
        returns a context-graph which represents the algorithm analysis results on the input command. *)
    member x.analyse(c : Core.Cmd) : ContextGraph.graph =
            (* a global identifier which is updated (at the beginning of the algorithm execution)
            to hold the number of variables in the analysed program. *)
        let numVars = ref 0;
        (* an iterator for debug print-out which is increased on each analysis interation over a loop body. *)
        let itCount = ref 0;
        (* debug mode -  when true - each algorithm stage will be printed, along with its output (and sometimes input). *)
        (* Sends s to the any debug info added event listener. *)
        let debugPrint(s) = if (!Debug) then debugInfoAdded.Trigger(DebugInfoAddedEventArgs(s))

        let debugPrintG(g) = if (!Debug) then debugPrint(ContextGraph.prtEdges(g))
        (* returns flow i-(1)->i if i is not in source context and i <> x *)
        let computeFlowFromItoI(c : CoreEx.Cmd, i : int, x : int, srcContext : ContextGraph.Context) =
            if (i <> x && (not (ContextGraph.inContext(i,srcContext)))) then [(i,i,AbstractDomain.copy,CoreEx.pat(c))] else [];

        (* computes context graph for commands of the form "X := 0" *)
        let computeAsgnZeroGraph(c : CoreEx.Cmd, x : int, preContexts : ContextGraph.Context list) : ContextGraph.graph =
            let computeDataFlows(srcContext : ContextGraph.Context) : (sparseMatrix.DataFlow) list =
                let rec computeMultipleFlows = function
                    | (0,_) -> []
                    | (i : int, srcContext : ContextGraph.Context) ->
                        computeFlowFromItoI(c,i,x,srcContext) @ computeMultipleFlows(i-1,srcContext);

                computeMultipleFlows((!numVars),srcContext)

            let computeEdge(srcContext : ContextGraph.Context) =
                (* create target context identical to source context, at least at first... *)
                let tgtContext = ContextGraph.copyContext(srcContext);
                (* include x in target context (equivalent to assignment of X := 0) *)
                let _ = ContextGraph.addVarToContext(x,tgtContext);
                let m = sparseMatrix.M(computeDataFlows(srcContext));

                ContextGraph.E ( srcContext, tgtContext, ref (setOfPairs.Dfr(m, sparseMatrix.r(m))) )

            ContextGraph.newGraph(List.map computeEdge preContexts)

        (* computes context graph for commands of the form "X := Y" *)
        let computeAsgnVarGraph(c : CoreEx.Cmd, x : int, y : int, preContexts : ContextGraph.Context list) : ContextGraph.graph =
            let computeDataFlows(srcContext : ContextGraph.Context) : (sparseMatrix.DataFlow) list =
                let computeFlowFromYtoX(i : int, srcContext : ContextGraph.Context)  =
                    if (i = y && (not (ContextGraph.inContext(y, srcContext)))) then
                        [(y,x,AbstractDomain.copy,CoreEx.pat(c))]
                    else
                        [];

                let rec computeMultipleFlows = function
                    | (0,_) -> []
                    | (i : int, srcContext : ContextGraph.Context) ->
                            let flowYtoX = computeFlowFromYtoX(i,srcContext);
                            let flowItoI = computeFlowFromItoI(c,i,x,srcContext);
                            flowYtoX @ flowItoI @ computeMultipleFlows(i-1, srcContext)

                computeMultipleFlows((!numVars), srcContext)

            let computeEdge(srcContext : ContextGraph.Context) =
                (* create target context identical to source context, at least at first... *)
                let tgtContext = ContextGraph.copyContext(srcContext);
                let y_in_srcContext = ContextGraph.inContext(y, srcContext);
                (* add x to target context if y is in source context (equivalent to assignment of X := 0),
                    otherwise exclude x from target context (equivalent to assignment of X := Y, where Y <> 0) *)
                let () = ContextGraph.setVarInContext(x, tgtContext, y_in_srcContext);
                let m = sparseMatrix.M(computeDataFlows(srcContext));

                ContextGraph.E ( srcContext, tgtContext, ref (setOfPairs.Dfr(m, [])) )

            ContextGraph.newGraph(List.map computeEdge preContexts)

        (* computes context graph for commands of the form "X := Y * Z" *)
        let computeAsgnTimesGraph(c : CoreEx.Cmd, x, y, z, preContexts) : ContextGraph.graph =
            let computeDataFlows(srcContext : ContextGraph.Context) : (sparseMatrix.DataFlow) list =
                let computeSingleFlow(i : int, srcContext : ContextGraph.Context) : (sparseMatrix.DataFlow) list =
                    (* add flow y-(2)->x (or z-(2)->x) if y and z are both not in the source context (equivalent to assignment of X := Y*Z where Y>0 and Z>0 ) *)
                    let computeFlowFromYandZtoX(i : int, srcContext : ContextGraph.Context) =
                        if ( (i = y || i = z) &&
                                (not (ContextGraph.inContext(y, srcContext) || ContextGraph.inContext(z, srcContext))) )
                        then [(i,x,analysis_params.nonlinear_Dvalue,CoreEx.pat(c))]
                        else [];

                    computeFlowFromYandZtoX(i,srcContext) @ computeFlowFromItoI(c,i,x,srcContext)

                let rec computeMultipleFlows = function
                    | (0,_) -> []
                    | (i : int, srcContext : ContextGraph.Context) ->
                        computeSingleFlow(i, srcContext) @ computeMultipleFlows(i-1, srcContext);

                computeMultipleFlows((!numVars), srcContext)

            let computeEdge(srcContext : ContextGraph.Context) =
                (* create target context identical to source context, at least at first... *)
                let tgtContext = ContextGraph.copyContext(srcContext);
                let y_or_z_in_srcContext = (ContextGraph.inContext(y, srcContext)) || (ContextGraph.inContext(z, srcContext));
                (* add x to target context if  y or z are in the source context (equivalent to assignment of X := 0),
                    otherwise exclude x from target context (equivalent to assignment of X := Y * Z, where Y>0 and Z > 0) *)
                let _ = ContextGraph.setVarInContext(x, tgtContext, y_or_z_in_srcContext);
                let mat = sparseMatrix.M(computeDataFlows(srcContext));

                ContextGraph.E ( srcContext, tgtContext, ref (setOfPairs.Dfr(mat, [])) )

            ContextGraph.newGraph( List.map computeEdge preContexts )

        (* computes context graph for commands of the form "X := Y + Z" *)
        let computeAsgnPlusGraph(c : CoreEx.Cmd, x, y, z, preContexts) : ContextGraph.graph =
            let computeDataFlows(x : int, y : int, z : int, srcContext : ContextGraph.Context) : (sparseMatrix.DataFlow) list =
                let computeSingleFlow(i : int, srcContext : ContextGraph.Context) : (sparseMatrix.DataFlow) list =
                    (* add flow y-(1')->x (or z-(1')->x) if y (or z) are not in the source context (equivalent to assignment of X := Y+Z where Y>0 or Z>0 ) *)
                    let computeFlowFromYandZtoX(i : int, srcContext : ContextGraph.Context) =
                        let iNotInSrcContext = not (ContextGraph.inContext(i,srcContext))
                        let yInSrcContext = ContextGraph.inContext(y, srcContext)
                        let zInSrcContext = ContextGraph.inContext(z, srcContext)

                        if (i = y || i = z) then
                            if (iNotInSrcContext && (not (yInSrcContext && zInSrcContext))) then
                                if ((not yInSrcContext) && (not zInSrcContext)) then
                                    if y = z then
                                        [(i,x,AbstractDomain.polynomial,CoreEx.pat(c))] (* when the same var is added then we deduce polynomial growth *)
                                    else
                                        [(i,x,AbstractDomain.additive,CoreEx.pat(c))]
                                else
                                    [(i,x,AbstractDomain.copy,CoreEx.pat(c))]
                            else []
                        else []

                    computeFlowFromYandZtoX(i, srcContext) @ computeFlowFromItoI(c, i, x, srcContext)

                let rec computeMultipleFlows = function
                    | (0, _) -> []
                    | (i : int, srcContext : ContextGraph.Context) ->
                            computeSingleFlow(i, srcContext) @ computeMultipleFlows(i-1, srcContext);

                computeMultipleFlows((!numVars),srcContext)

            let computeEdge(srcContext : ContextGraph.Context) =
                (* create target context identical to source context, at least at first... *)
                let tgtContext = ContextGraph.copyContext(srcContext);
                let y_and_z_in_srcContext = (ContextGraph.inContext(y, srcContext)) && (ContextGraph.inContext(z, srcContext));
                (* add x to target context if  y and z are both in the source context (equivalent to assignment of X := 0),
                    otherwise exclude x from target context (equivalent to assignment of X := Y + Z, where Y>0 or Z > 0) *)
                let _ = ContextGraph.setVarInContext(x, tgtContext, y_and_z_in_srcContext);
                let m = sparseMatrix.M(computeDataFlows(x,y,z,srcContext));

                ContextGraph.E ( srcContext, tgtContext, ref (setOfPairs.Dfr(m, sparseMatrix.r(m))) )

            ContextGraph.newGraph( List.map computeEdge preContexts )

        (* updates DFRs on all edges of graph g with all possible data flows of the form (i->j,i'->j'). *)
        let computeDoubleFlows(g : ContextGraph.graph) =
            let updateDoubleFlowsOnEdge = function
                | ( ContextGraph.E(p, q, refDfr) ) ->
                    (* filter letction to determine if a given double data flow should be included in the result *)
                    let includeFlow (p : ContextGraph.Context,q : ContextGraph.Context) ((i,j),(i',j'),pat) =
                                    (not (ContextGraph.inContext(i,p))) && (not (ContextGraph.inContext(i',p))) &&
                                    (not (ContextGraph.inContext(j,q))) && (not (ContextGraph.inContext(j',q))) &&
                                    (i <> i' || j <> j');
                    match !refDfr with
                    | (setOfPairs.Dfr(m,_)) as dfr ->
                            (* filter double flows according to source and target contexts *)
                            let r' = List.filter (includeFlow(p,q)) (sparseMatrix.r(m));
                            refDfr := setOfPairs.Dfr(m,r')
                | _ ->  failwith "NaiveAnalysis.updateDoubleFlowsOnEdge: Invalid argument."

            List.iter updateDoubleFlowsOnEdge (ContextGraph.edges(g))

        (* computes a graph corresponding to the abstract interpretation of an assignment command, with given pre-contexts *)
        let computeAssignmentGraph (c : CoreEx.Cmd, x : int, e : Core.Expr, preContexts : ContextGraph.Context list) : ContextGraph.graph =
            (* computes data flows of the form i-(d)->j *)
            let computeSingleFlows (x : int, e : Core.Expr, preContexts : ContextGraph.Context list) : ContextGraph.graph =
                match e with
                | Core.Zero ->                          computeAsgnZeroGraph(c, x, preContexts)
                | Core.Var y ->                          computeAsgnVarGraph(c,x, y, preContexts)
                | Core.Times(Core.Var y, Core.Var z) -> computeAsgnTimesGraph(c, x, y, z, preContexts)
                | Core.Plus(Core.Var y , Core.Var z) -> computeAsgnPlusGraph(c, x, y, z, preContexts);
                | _ -> failwith "NaiveAnalysis.computeAssignmentGraph: Invalid argument."

            let g' = ref (computeSingleFlows(x, e, preContexts));
            (* computes all data flows of the form (i->j,i'->j') over the flows calculated for all edges of the graph g' *)
            let () = computeDoubleFlows(!g');
            !g'

        (* a global ientifier which holds a list of all contexts - for ease of reference anywhere in the algorithm. *)
        let allContexts = ref ([ContextGraph.makeEmptyContext(1)]);

        (* the algorithm entry point - gets as input a command c and a list of pre-contexts and
           returns the context-graph which corresponds to the command c. *)
        let rec naive(c : CoreEx.Cmd, preContexts : ContextGraph.Context list) : ContextGraph.graph =
                (* Applies the loop correction operator on the context-graph g, according to loop rule L2 from the DICE paper. *)
                let rec doLoopCorrection(l : int, g : ContextGraph.graph) : ContextGraph.graph =
                        (* overload the * operator for DFRs for ease of expressiveness of the DFR composition (in this function only). *)
                        let (*) (d1 :setOfPairs.DFR) (d2 :setOfPairs.DFR) = setOfPairs.prod(d1,d2);

                        (* applies the loop correction operator on a DFR *)
                        let rec LC(l,setOfPairs.Dfr(m,r)) =
                            let m' = sparseMatrix.LC (l, analysis_params.nonlinear_Dvalue, CoreEx.id(c)) m;
                            setOfPairs.Dfr(m', setOfPairs.filterR(r,m'))

                        (* computes LC on all edges (p,q') s.t. (p,q), (q,q') and (q,q) exist on graph.
                           The result of this function is *)
                        let rec computeSingleEdge = function
                            | ( _, []) -> []
                            | ((ContextGraph.E (p,q,d)) as e, (ContextGraph.E(p',q',d'))::t) ->
                                (if (ContextGraph.eqContexts(q,p')) then
                                    (match ContextGraph.getEdgeTag(g,ContextGraph.UE (q,q)) with
                                                    Some dfr -> [(ContextGraph.E (p,q', ref ( !d * LC(l, !dfr) * !d' ) ))]

                                                  | None     -> [])
                                 else []) @ computeSingleEdge(e, t);
                            | _ -> []

                        let rec computeMultipleEdges = function
                            | ([],_) -> []
                            | (e::t, fullEdgeList) ->
                                    computeSingleEdge(e,fullEdgeList) @ computeMultipleEdges(t,fullEdgeList);

                        let sortedEdges = ContextGraph.sortEdges(ContextGraph.edges(g));

                        let () = ContextGraph.addEdges(g, computeMultipleEdges(sortedEdges, sortedEdges), false);
                        g

                (* computes a single iteration of a loop whose body is represented by the graph g (after some m >= 0 iterations). *)
                let rec doSingleIteration (g : ContextGraph.graph ref) g'  =
                        let () = debugPrint("================================\nIteration #" + (!itCount).ToString() + ":\ncurrent graph(g):\n");
                        let () = debugPrintG(!g)
                        let () = debugPrint("graph to compose(g'):\n")
                        let () = debugPrintG(g')
                        let g'' = !g @@ g'
                        let () = debugPrint("composed graph(g''):\n")
                        let () = debugPrintG(g'')
                        let () = g := !g ||| g' ||| g''
                        let () = debugPrint("join result graph(g):\n")
                        let () = debugPrintG(!g)
                        let () = debugPrint("================================\n")
                        let () = itCount := !itCount + 1;
                        !g

                (* computes the result graph of any m > 0 iterations, where the input graph is the graph representing the loop-body and
                   the possibility of 0 iterations (skip). This function corresponds to loop rule L1 from the DICE paper. *)
                let rec doLoopClosure(x : int, g : ContextGraph.graph ref) : ContextGraph.graph =
                        let rec lfp f (g : ContextGraph.graph) =
                                let fg = (f g);
                                if (ContextGraph.equal(fg,g)) then g else lfp f fg

                        let g' = ContextGraph.newGraph(ContextGraph.edges(!g));
                        let () = itCount := 0;
                        lfp (doSingleIteration g) g'

                (* Computes the result graph of a loop whose body is represented by g and the iterating variable is x. *)
                let rec doLoop(x : int, g : ContextGraph.graph ref) : ContextGraph.graph =
                        (* the context graph g is joined with a graph which corresponds to the Skip command with the same pre-contexts.
                           This action corresponds to applying loop rule L0 from the DICE paper. *)
                        let () = g := ContextGraph.joinAsLeastUpperBound (!g) (naive(CoreEx.NaiveCmd(CoreEx.Skip,-1), ContextGraph.preContexts(!g)))
                        doLoopCorrection(x, doLoopClosure(x, g))

                let rec recurse(CoreEx.NaiveCmd(c,_) as c' : CoreEx.Cmd, preContexts : ContextGraph.Context list) =
                    let g = match c with
                            | CoreEx.Seq(c1,c2)      ->
                                                            let g1 = naive(c1, preContexts);
                                                            let g2 = naive(c2, ContextGraph.postContexts(g1));
                                                            g1 @@ g2

                            |  CoreEx.Choice(c1, c2)  -> naive(c1, preContexts) ||| naive(c2, preContexts)
                            |  CoreEx.Skip           -> computeAssignmentGraph(c', 1, Core.Var 1, !allContexts)
                            |  CoreEx.Asgn(i, e)     -> computeAssignmentGraph(c', i, e, !allContexts)
                            |  CoreEx.Loop(i, c')     -> doLoop(i, ref (naive(c', preContexts)));
                    commandGraphUpdated.Trigger(CommandGraphUpdatedEventArgs(c', g))
                    g

                let () = debugPrint("starting to analyse command:\n");
                let () = debugPrint(CoreEx.prt(c));
                let () = debugPrint("Pre-contexts: " + ContextGraph.prtContexts(preContexts) + "\n");
                let g = recurse(c, preContexts);
                let () = debugPrint("Finished analysing command:\n");
                let () = debugPrint(CoreEx.prt(c));
                let () = debugPrint("graph:\n");
                let () = debugPrintG(g);
                let () = debugPrint("============================================\n");
                g

        let () = (numVars := Core.NumOfVars(c));
        let () = allContexts := ContextGraph.allContexts(!numVars)
        naive(CoreEx.extendedNaiveAST(c),[])

    member x.resultText(c, g : ContextGraph.graph) =
        let vars = Core.NumOfVars c
        let bounded = ref [1..vars]
        let vt = Parser.parserLastVarToIndexMap()

        let rec prt_ints  = function
            | [] -> "\n"
            | i::rest -> let varFound = vt.ContainsKey(i)
                         (if varFound then vt.[i] else "") + (if varFound && rest<>[] then ", " + (prt_ints rest) else "\n")

        let removeNonBounded(b, nb) =
            List.filter (fun x -> not (List.exists (fun y -> x=y) nb)) b

        for p in g.Keys do
            for et in g.[p].Values do
                match !et with
                    | (setOfPairs.Dfr(M,_)) ->
                            let (notbounded', _) = sparseMatrix.classify(M,vars, AbstractDomain.exponentialAtLeast)
                            bounded := removeNonBounded(!bounded, notbounded')
        let nonbounded = List.filter (fun v -> not (List.exists (fun v' -> v'=v) !bounded)) [1..vars]
        ("\n\nVARS: " + (vars.ToString()) + "\n" + analysis_params.name + ": " +
                 (prt_ints !bounded) + ("NON-" + analysis_params.name + ": ") + (prt_ints nonbounded))

    (* set the debug output mode *)
    member x.setDebugMode(mode : bool) = Debug := mode

let Poly = NaiveAnalysis(Analysis.PolyParams())

let Lin = NaiveAnalysis(Analysis.LinParams())       